\begin{tabbing}
es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;$B$;${\it ds}$;$e$.$P$($e$);$e$.$f$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$e$:es{-}E(${\it es}$). (es{-}kind(${\it es}$; $e$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $B$))\+
\\[0ex]\& ($\forall$$x$:Id. es{-}vartype(${\it es}$; source($l$); $x$) $\subseteq$r fpf{-}cap(${\it ds}$;IdDeq;$x$;Top)))
\\[0ex]c$\wedge$ \=(alle{-}at(${\it es}$;source($l$);$e$.$P$($e$)\+
\\[0ex]$\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd) c$\wedge$ (es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$)))))
\-\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex](es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ ($P$(es{-}sender(${\it es}$; ${\it e'}$)) c$\wedge$ (es{-}val(${\it es}$; ${\it e'}$) = $f$(es{-}sender(${\it es}$; ${\it e'}$)) $\in$ $B$)))
\-\\[0ex]\& (\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex](es{-}kind(${\it es}$; ${\it e'}$) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]$\Rightarrow$ \=($\forall$${\it e''}$:es{-}E(${\it es}$).\+
\\[0ex]($\uparrow$es{-}isrcv(${\it es}$; ${\it e''}$))
\\[0ex]$\Rightarrow$ (es{-}lnk(${\it es}$; ${\it e''}$) = $l$ $\in$ IdLnk)
\\[0ex]$\Rightarrow$ (es{-}sender(${\it es}$; ${\it e''}$) = es{-}sender(${\it es}$; ${\it e'}$) $\in$ es{-}E(${\it es}$))
\\[0ex]$\Rightarrow$ (${\it e''}$ = ${\it e'}$ $\in$ es{-}E(${\it es}$)))))
\-\-\-\-
\end{tabbing}